state after $e$$\backslash\backslash$$x$($y$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if $y$ = $x$$\rightarrow$ $\cdot$ else ($y$ after $e$) fi